﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace TruthTree2.PC.Resolution
{
    public class CNFClause
    {
        public List<CNFAtom> Atoms;

        public CNFClause()
        {
            Atoms = new List<CNFAtom>();
        }

        public void Add(CNFAtom atom)
        {
            Atoms.Add(atom);
            Atoms.Sort((a, b) => { return a.ToString().CompareTo(b.ToString()); });
        }

        public override string ToString()
        {
            return "{" + String.Join(", ", Atoms) + "}";
        }

        public override int GetHashCode()
        {
            return ToString().GetHashCode();
        }

        public static CNFClause Resolve(CNFClause a, CNFClause b)
        {
            HashSet<CNFAtom> atoms = new HashSet<CNFAtom>();
            foreach (CNFAtom at in a.Atoms) { atoms.Add(at); }
            foreach (CNFAtom at in b.Atoms) { atoms.Add(at); }

            CNFClause res = new CNFClause();
            List<CNFAtom> resolvents = new List<CNFAtom>();
            foreach (CNFAtom at in atoms)
            {
                bool negated = false;
                foreach (CNFAtom at2 in atoms)
                {
                    if (at.Atom == at2.Atom && at.Negated != at2.Negated)
                    {
                        negated = true;
                        break;
                    }
                }

                if (negated) { continue; }

                res.Add(at);
            }

            return res;
        }
    }
}
